Formalization of the fundamental group in untyped set theory using auto2

摘要

We present a new framework for formalizing mathematics in untyped set theoryusing auto2. Using this framework, we formalize in Isabelle/FOL the entirechain of development from the axioms of set theory to the definition of thefundamental group for an arbitrary topological space. The auto2 prover is usedas the sole automation tool, and enables succinct proof scripts throughout theproject.